COMP2111
System Modelling and Design
Term 1, 2024

Notes (Week 1 Monday)

These are the notes I wrote during the lecture.

*Sets* are (informally) collections of *elements*

Sets come with a *membership relation*

  ∈

  If x is an element,
  and if S is a set,
  then

      x ∈ S   "x in S" or "x is an element of S"

  is true iff x is one of the elements of S


  One way to define sets is by *explicit enumeration*

        {1,2,3}  denotes the set with exactly three elements,
                 namely:  1, 2 and 3

     1 ∈ {1,2,3}     <--- true statement
     4 ∈ {1,2,3}     <--- false statement


    ∩   "intersection"


  {1,2,3} ∩ {4,5,6} = {}

   {1,2,3} ∩ {3,4,5} = {3}


  {1,2,3} ∪ {3,4,5} = {1,2,3,4,5}


  {1,2} ⊆ {1,2,3}    <--- true statement
  {1,2,3} ⊆ {1,2}    <--- false statement

Q: How is subset (⊆) not like union (∪) and intersection (∩)?

A: The "types" are different.

     ∪,∩ are binary operators on sets

     ∪  : Set × Set → Set
     ∩  : Set × Set → Set
     ⊆  : Set × Set → Bool

     S ∪ T  is a set, if S and T are sets

     but S ⊆ T "S is a subset of T" is a truth claim about sets,
      but it's not a set itself.

Prove:
  A ⊆ A ∪ B
Proof:
  By the definition of ⊆,
  it suffices to prove the following
  for an arbitrary but fixed A

   if x ∈ A holds, then x ∈ A ∪ B holds

  By definition of ∪, it suffices to instead prove:

   if x ∈ A holds, then either x ∈ A *or* x ∈ B holds

  The desired result follows immediately by disjunction introduction.
QED

Disjunction introduction is the following proof rule:
  (will be covered later in the course)

  If A holds, then A ∨ B  ("A or B") holds
  If B holds, then A ∨ B  ("A or B") holds
  ^ confusingly, these are both called disjunction introduction

Q: Why are we being so pedantic?
A: (Clue) things can look obvious despite not being true,
          and we want to make sure things both look obvious
          and in fact *are* obvious

*Set comprehensions* are expressions of the following form:

  {x | P(x)}   <--- where P is a predicate (aka a truth claim)
                    about elements

  {x | P(x)}  "the set of all x such that P(x) holds"


  {x | x ∈ ℕ and x < 2} = {0,1}

  {x | x ∈ ℕ and x is odd} = {1,3,5,...}

Q: Are we considering 0 as a natural number?
A: Yes. Computer scientists generally start counting from 0.
   Some people don't consider 0 to be natural (that is, they say 0 ∉ ℕ)
   These people are usually either mathematicians or crazy.


General principle: extensionality.

  We consider two sets to be equal,
   iff we can't distinguish them through the membership relation

       S  =  T

        iff

      ∀x. x ∈ S  iff x ∈ T


...and by the principle of extensionality,

   {y | y ∈ x}  = x


We can have sets of sets

   {{},{1,2}}   <-- totally valid set

Therefore, sets can be elements of sets,
 so there should be nothing stopping us from *saying*

   x ∈ x    provided x is a set

Q: I think the axiom of regularity
   prohibits sets containing themselves?
A: We're not doing ZFC in this course,
   if you've never heard of the regularity axiom,
   don't worry.

   Yes, that's correct.
   But it doesn't prevent us from writing the expression.

Q:  {} ∈ {}  ?
A: In order for this to be true,
    {} would have to be one of the elements of {}.
   But: {} has no elements; hence it's not.

   But, these are true:
      {} ∈ {{}}
      {} ⊆ {}

Q: why does this matter?

A: Logically inconsistent to define sets from arbitrary predicates

   One way to do logical proof is: proof by contradiction.

   To prove A,   we assume that A is false, and derive
                 a contradiction from that assumption.

   If we have Russell's paradox, we can prove everything!

   To prove A,
      assume that A is false,
      derive a contradiction using Russell's paradox,
      conclude the proof by contradiction.

    ^ this means that our logic is useless
      (the technical term is: it's inconsistent)

   This is why we're being so pedantic!
   In order for our formal modelling of systems to mean anything,
    we should be doing it in a logical framework that doesn't have
    these paradoxes.


   + is a function symbol of arity 2,
     because + expects two arguments,
     and if you give it two terms (numbers)
     then you get a term back

   ! would have arity 1


Because simple formulas are built on top of terms (remember: layers),
  we can't use simple formulas as arguments to themselves:


      3 = 5      <-- that's a simple formula

      3 = (x+1) <-- also a simple formula

      (3 = 4) = (1 = 1)   <-- not a simple formula
                              the arguments to = need to be terms,
                              not themselves simple formulas

Q: Is this formula true or false?
    n! = n  ↔  (n = 1 ∨ n = 3)

A: 3! is not in fact 3
   that is: the LHS is false, but the RHS is true

A: It depends. It depends on the value of n.

   If I'm using this formula in a context where n happens to be 3,
   then the formula as stated is false.

   On the other hand: if n happens to 1, it's true.

The point:

   Formulas on their own aren't necessarily true or false.
   Instead: formulas in general only get a truth value
     when we put them in a context
       aka an environment
       aka a valuation
       aka a mapping from variables to values

   This formula:

      ∀n. (n! = n  ↔  (n = 1 ∨ n = 3))

      ^ this formula happens to have a truth value that's
        independent of the context

2024-04-19 Fri 10:38

Announcements RSS